Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    D(t)  → 1
2:    D(constant)  → 0
3:    D(x + y)  → D(x) + D(y)
4:    D(x * y)  → (y * D(x)) + (x * D(y))
5:    D(x - y)  → D(x) - D(y)
6:    D(minus(x))  → minus(D(x))
7:    D(div(x,y))  → div(D(x),y) - div(x * D(y),pow(y,2))
8:    D(ln(x))  → div(D(x),x)
9:    D(pow(x,y))  → ((y * pow(x,y - 1)) * D(x)) + ((pow(x,y) * ln(x)) * D(y))
There are 12 dependency pairs:
10:    D#(x + y)  → D#(x)
11:    D#(x + y)  → D#(y)
12:    D#(x * y)  → D#(x)
13:    D#(x * y)  → D#(y)
14:    D#(x - y)  → D#(x)
15:    D#(x - y)  → D#(y)
16:    D#(minus(x))  → D#(x)
17:    D#(div(x,y))  → D#(x)
18:    D#(div(x,y))  → D#(y)
19:    D#(ln(x))  → D#(x)
20:    D#(pow(x,y))  → D#(x)
21:    D#(pow(x,y))  → D#(y)
The approximated dependency graph contains one SCC: {10-21}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.14 seconds)   ---  May 3, 2006